Nuprl Definition : dset
13,42
postcript
pdf
DSet == {
s
:PosetSig| IsEqFun(|
s
|;=
)}
latex
clarification:
DSet{i} == {
s
:PosetSig{i}| IsEqFun(|
s
|;=
s
)}
latex
Up
sets
1
Wellformedness Lemmas
dset
wf
Definitions
PosetSig
,
IsEqFun(
T
;
eq
)
,
|
p
|
,
=
origin
)}
s)} )}
s)}